COMMENT ⊗   VALID 00008 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.SS(Intoduction)
C00029 00003	We complete this section with a brief discussion of the pure λ-calculus
C00046 00004	.SS(Towards a Mathematical Semantics,,P85:)
C00059 00005	Let us begin to relate these intuitions to our discussion of 
C00068 00006	Then, for example, the
C00082 00007	To describe the evaluation of a function-call in LISP we must add
C00087 00008	This will suffice for our current λ-definitions we need not modify %dl%*
C00113 ENDMK
C⊗;
.SS(Intoduction)
The point of the following section is to introduce the computer science
student to some of the more theoretical areas of his province and
similarly to convince the mathematically inclined that there are
interesting and challenging problems concerning the foundations
of computer science. 

We will use our experience in LISP as a starting point. It perhaps
seems presumptuous to base a theoretical discussion on knowledge of a  
programming language, but as we will see there is much more to LISP than
its use in  symbolic programming. In particular, LISP can be used to introduce
the general area of recursion theory.  For example, one of the
fundamental results in recursion theory, is the proof of the non-existence
of an algorithm to determine whether or not a function was total.
The existence of such a function would certainly have made our life
more pleasant. Alas, a predicate, call it %3total%*, does not exist as we
shall now establish.

The proof depends on our knowledge about the function %3apply%*. The fundamental
relationship is:

.BEGIN INDENT 10,10;
For a function %3f%* and arguments %3a%41%1,#...#,%3a%4n%1 we know
that if 
.BEGIN CENTER;
%3f[a%41%3;#...;a%4n%3]%1 is defined then 
%3f[a%41%3;#...;a%4n%3]%1 =  %3apply[%eR%f(%3f%f)%3list[%eR%f(%3a%41%f)%3;#...;%eR%f(%3a%4n%f)%3];env]%1
.END
This omniscient property of %3apply%* makes it a %2⊗→universal function↔←%* for
LISP. That means that if %3apply%* is given an encoding of a function, of
some arguments to be applied, and an environment which contains 
the definition of %3f%* and all the
necessary subsidiary definition needed by %3f%*, then %3apply%*
can simulate the behavior of %3f%*. 

.END
For sake of concreteness in this 
discussion we will assume that the representation of %3env%* is 
a list of dotted pairs: representation of name dotted with representation 
of λ-expression. Given a function named %3g%*, together with its λ-definition
will designate the S-expr representation as %3g%8*%1.

Then if %3f%* uses %3f%41%1 through %3f%4n%1 as subsidiary
we will represent the environment as:
.BEGIN CENTER; SELECT 3;
list[f%8*%3;f%41%8*%3;...;f%4n%8*%3]
.END

Now assume the existence of a unary predicate %3total%* such that:
.BEGIN TABIT1(10);
\|gives %et%* if %3x%* is a representation of a total unary⊗↓This discussion 
will nominally concern unary functions; the generalization is obvious.←function.
%3total[x]%1 <
\|gives %ef%1 in all other cases.
.END

Notice that if %3total[list[f%8*%3;#...]%1 is true, then for arbitrary %3a%*
we will have %3apply[name[f%8*%3];list[a];#list[f%8*%3;#...]]%1 terminating and
giving value %3f[a]%*.

Now we define a function:
.BEGIN SELECT 3;CENTER;
diag[x] <= [total[x] → list[apply[name[first[x]];list[x];x]]; %et%* → %ef%*]
.END
This mild-mannered function is total. Let's form %3diag%8*%1:
.BEGIN SELECT 3;NO FILL;
(DIAG . 
   (LAMBDA (X)
           (COND ((TOTAL X) (LIST (APPLY (NAME (FIRST X))(LIST X) X)))
			   (T NIL))) )
.END
Finally form %3zowie%* = %3list[diag%8*%3; total%8*%3; apply%8*%3; ...]%1. That is
%3zowie%* will be the representation of %3diag%* and all its necessary
functions.

Evaluate %3diag[zowie]%*. Since %3diag %2is%1 total, then %3total[zowie]%* is
true, and we are faced with
.BEGIN CENTER; SELECT 3;

diag[zowie] = list[apply[name[first[zowie]];list[zowie];zowie]]
.END
but %3name[first[zowie]] = DIAG%1; and therefore the call on %3apply%* reduces
to 
%3apply[DIAG;list[zowie];zowie]%*. But that's just %3diag[zowie]%*, and we've
shown %3daig[zowie]#=#list[diag[zowie]]%1. That's just not possible. Thus the
assumption of the existence of %3total%* must be in error.

The typical proof of this result involves encoding the functions in the integers
and then expressing  the equivalent of the %3apply%* function as an algorithm in
number theory. 
The trick of encoding on the integers is analogous to what %2we%* did
in encoding in the S-expressions. 
The presentation in LISP is much more understandable. It's the old problem of
representation again. Mapping to number theory is too representation dependent;
we seldom need properties of the integers.

Thus LISP %2is%* more than a programming language; its a formalism for discussing
computation as well⊗↓Indeed, LISP was originally meant
to be a formalism for problems in Artificial Intelligence; 
S. Russell suggested to McCarthy that LISP could be turned into a 
language for a machine.McCarthy had doubts, but Russell prevailed.←. 
This chapter exposes several of the more theoretical
applications of LISP-like languages.

In {yonss(P90)}  we talked about the meaning of "<=" and the pitfalls 
of interpreting it as a generalized assignment statement. Basically we saw 
that we couldn't separate the name of the function from its body if we were
describing recursive procedures. As fortune would have it, LISP's %3label%*
operator would %2not%* allow us to separate the name from the body.
So we were safe then, but curiosity really should prod us to understand the
phenomomon a bit better now.

Our hint
comes from our interpretation of "<=" as an equality. I.e., recall:

.BEGIN CENTER;SELECT 3;TURN OFF "←";

fact ← %1a solution to the equation:%* f = λ[[x][x=0 → 1;%et%* → *[x;f[x-1]]]].
.END
What we need is a representation of an "equation-solver" which will
take such an equation as input and will return as value a function
which satisfies that equation. In particular we would like the %2best%* 
solution in the sense that it requires the minimal structure on the 
function⊗↓Like a free group satisfies the group axioms, but imposes no other
requirements.←.
This request for minimality translates to finding the function which
satisfies the equation, but is least-defined on other elements of the
domain.
Consider the following LISP definition:

.BEGIN CENTER;SELECT 3;

f <= λ[[n][n=0 → 0;%et%* → f[n-1] + 2*n -1]]
.END

.BEGIN TURN ON "#";
When we are asked what this function is doing, most of us would proceed
operationally; that is, we would begin computing %3f[n]%* for different
values of %3n%* --what#is#%3f[0]?%*,
 what is %3f[1]%1,#...#. It is profitable to look at this process differently:
what we are doing is looking  at a %2sequence%* of functions,
call them %3f%4i%1's .
.END

.BEGIN TABIT3(10,16,44);SELECT 3;GROUP;TURN OFF "{","}";

\f%40%1 =\%3{%3<0,%9B%*>,<1,%9B%*>, ... }\%1when we begin, we know nothing.
\%3f%41%1 =\%3{<0,0>,<1,%9B%*>, ... }\%1now we know one pair.
\%3f%42%1 =\%3{<0,0>,<1,1>, ... }\%1now two
\%3f%43%1 =\%3{<0,0>,<1,1>,<2,4>, ... }\%1now three

\ ...\           ...          ...\%dEureka!!
.END

When (if) the sudden realization strikes us that the LISP function is
"really" (denotationally)  %3n%82%1, on the non-negative integers, 
then we may either take
that insight on faith or subject it to proof. The process of discovering
the denotation  can be construed as a limiting process which creates 
the least-defined function satisfying the LISP definition. That is:

.BEGIN CENTER;SELECT d;

%3λ[[n]n%82%3]%1 = %1least upper bound of%3 f%4i%1's;
.END
where %3f%4i%1 may also be characterised as:

.BEGIN TABIT1(12);SELECT 3;group;

\ %1|%3 n%82%1 if %30%c≤%3n%c≤%3i
f%4i%3(n)%1 =\<
\ | %9B%1 if %3i%c<%3n

.END

We may think of our "equation-solver" as proceding in such a manner.
Though it is not at all obvious, such an equation solver
exists, it %2does%* and 
is called the %2⊗→fixed-point operator↔←%*.

In terms of our example we want a solution to %3f = %9t%3(f)%1, where:

.BEGIN CENTER;
%9t%3(g) = λ[[n][n=0 → 0; %et%* → g[n-1] + 2*n -1]]%1
.END

Our previous discussion leads us to believe that
%3λ[[n]n%82%3] %1for %3n %c≥%30%1 is the desired solution.

.BEGIN TURN ON "#";

How does this discussion relate to the sequence of functions %3f%4i%1?
The simplest function is the totally undefined function,%9B%*#⊗↓We 
perhaps should subscript %9B%* to distinguish it from previous %9B%*'s.←.


.BEGIN CENTER;
%9t%3(%9B%*) = %3λ[[n][n=0 → 0;%et%* → %9B%*[n-1]+2*n-1]]%1,
.END
but this says %9t%3(%9B%*)%1 is just %3f%41%1!
Similarly,
.BEGIN CENTER;
%9t%3(%9t%3(%9B%*)) = %3λ[[n][n=0 → 0;%et%* → f%41%*[n-1]+2*n-1]]%1,
.END
is just %3f%42%1.
Thus, writing %9t%8n%1 for the composition of %9t%1...%9t%1, n times, ⊗↓Define
%9t%80%1 to be the the totally undefined function, %9B%1.← we can say
.BEGIN CENTER;GROUP;

%3f%4n%* = %9t%8n%3(%9B%*)%1  or,

%3λ[[n]n%82%*]%1 = lim%4n=0 → ∞%9t%8n%3(%9B%3)%1.
.END

This whole discussion  is naturally subject to justification. We have
not supplied any of the technical details, but hopefully have supplied the
motivation for the study and have raised several questions about the
nature of the objects called functions. 
.BEGIN INDENT 10,10,10;
.CENT(An Aside:)
Before outlining  the  remainder of the material I would like to address the
point of formalism versus intuition.
I am a strong believer in intuiton and informality, particularly in the area
of computer science. The "science" is so new that to place a heavy technical
burden on the study of any of the newer branches is a diservice. The recent
work in mathematical semantic of programming languages does indeed draw on
strong mathematical lines, but it must be remembered that the study is %2not%*
formal mathematics; it is not toploogy; it is not algebra, it is not recursion
theory. The ultimate justification for the studies come from  problems
in computer science, and it is to those areas that we should go for motivation.
This is not to say that mathematics departments must become dispensers of tools
for computer science departments, any more than they are resident experts for
the engineering schools. But this is an era when students are asking for 
"relevance"; computer science is an area which is full of relevance, full
of interesting questions best described and approached by sophisticated
mathematical and logical tools. 

.END

We will  begin our investigations  with an examination of the concept of 
"function".  Fortunately much of the necessary  technical work has been
done; forturnately we can draw on our LISP experience both for motivation
and for technical expertise.
The basis of out study will be the λ-calculus, a formal language developed
by A. Church in an attempt to explicated the logical problems of function 
and function application.  We have used the %2notation%* in LISP; we have
%2not%* studied the language.

The syntax of the language is simpilicity itself: an expression is either
a variable, a λ-expression, or function application. 

.GROUP 6;

However, simplicity
is not always a virtue; since all we can generate are un-named λ-expressions
the expressions of the language become quite bulky. To turn it
into anything resembling a programming language, we must introduce 
abbreviations and simplification rules. This obviously brings up the question
of evaluation in λ-calculus.

The pragmatics or rules of evaluation in the language are  somewhat
different from LISP. Instead of call-by-value, we use 
substitution-and-simplification; it's closely related to call-by-name.
The  intital evaluation schemes are called reduction  rules and
basically allow renaming of dummy variables and substitution
of actual parameters for formal parameters⊗↓with appropriate reductions afterwards.←.
The two rules are called α-conversion, and β-conversion rules respectively.

.GROUP 6;

An expression is said to be in Normal Form whenever the only transformations
applicable are α-conversions.


Not all expressions have normal form; and the difficulty is that
some very useful expressions do not have normal form. Thus we cannot
simply remove them from consideration.
An investigstion of normal forms leads one to equate "non-normal form"
with "non-termination"; we will see that this is not a viable decision.
In the meantime we can establish some basic results about normal forms:
if two reduction sequences both lead to normal forms, are they the same?
answer: yes; if an expression has a normal form, do all reduction sequences
lead to it? answer: no; if there is a normal form for an expression, is
there a canonical way of finding it?; answer: yes; are two "distinct"
normal forms "different"? after characterizing "distict" and "different" the
answer is yes. When we look at expressions without %2any%* normal form
all bets are off. But first we will look at other evalaation mechanisms
for λ-calculus; in particualr we will look an "machines" similar to those
used by LISP. This will help tie the new material back to experience.

Then we get to non-normal forms: we cam exhibit two expressions,
call then Y%41%* and Y%42%* neither of which have normal forms, neither
of which are reducible to the other, but Y%41%* applied to any argument
gives the same value as Y%42%* applied to that argument. This causes a couple
of difficulties intellectually. We can also exhibit two expressions, I and J,
which will have the same computational effect, but I has a normal form
(it is the identity function) but J doesn't. More eyebrows raise when we
try to intuit self-applicative functions, f(f). Now we %2have%* seen 
such behavior in LISP and it have not caused trouble, but thought of in
the traditional set-theoretic manner, self application is troublesome.
Self-application %2is%* allowable in λ-calculus.

Typically in mathematics, when we cannot fully grasp a formal idea we
resort to model building; we attenpt to discover a particular structure
which satisfies the axioms and preserves truth under application of the
rules of inference. 
Here we will discuss the ideas of  formal systems and axiomatizations,
covering propositional and predicate calculus to the extent that we
expose the areas and understand the limitations of the formalisms.
We will discuss a completeness results and will show that much of the
work on basic undecidablilty is easily discussed using LISP.
Then we will indeed try to discover  a model for our calculus
but
simple models of function spaces which allow self application and the
other necessities of our calculus lead to dead-ends.

Another trick in problem-solving is to simplify the problem. We next try that.
Since self application is bothersome, we try to formaualte a dialect of
the calculus which will rule out this  behavior. We come up with
the %2typed%* λ-calculus. This means that each function and each variable
has associated with it a specific type; fucntions of type α→β for example
require argumetn of type α and will give results of type β. This calculus
rules out self application. It also rulse out many constructs which we 
intuitively want. However we presist. We %2can%* exhibit a model for this
formalism: this brings out the discussion of complete partial orders, continuous
functions and the like. It also reinforces some very early LISP discussions
concerning non-strict functions: those which can reach a value without
complete information on all of its arguments.

After a thorough discussion of typed λ-calculus, we ask what the relevance of all
this is to computer science. This brings up the questions of programming languagge
semantics. There are basically three schools: the axiomatic, the operational,
and the mathematical.  The operational school is typiified by LISP.
The discussion of the axiomatic approach brings up the questions of 
theorem-proving  and relates to our earlier discussion on mathematical logic.
Mathematical semantics is the business at hand: supplying mathematical 
models for programming languages. The deeper question of "why any of this?"
leads us to  the problems of correctness of programs and implementations of
such devices. Again our experience in LISP will be of great benefit;
most of the interesting work being done in this area is LISP-based.

The three semantic schools and our LISP work all come together nicely
in a discussion of the recent thesis of M. Gordon dealing with
models of  subsets of LISP.

The final topic for discussion is the construction of the model for the
(type-free) λ-calculus. We will do this by "lifting" the construction
of the typed model and turning it into a model for the type-free calculus.

The content of the course is designed to expose student of
either persuasion: mathematics or computer science; to the more
theoretical areas of the field. I would hope that it would
generate sufficient interest in both faculty and students that they could
persue the pieces which interest them. Little has been published on these
topics outside of underground papers and research notes. I see this
area of computer science as a fertile ground for a mathematics department;
in is computer science, but it requires expertise in an area which
an engineering department probably cannot supply.
We complete this section with a brief discussion of the pure λ-calculus
as compared to LISP's application. In the interest of readability, we will
write λ-calculus expressions in a Gothic bold-face type; e.g. %9λ%* and %dx%*
instead of LISP's  %3λ%* and %3x%*.

The syntax of (well-formed) %9λ%*-expressions is simple:

.BEGIN TABIT1(10);GROUP;

<wfe>	\::= %9λ%* <variable> %d.%* <wfe>
\::= <applic>
<applic>\::= <applic><atom>
\::= <atom>
<atom>\::= <variable>
\::= <constant>
\::= %d(%* <wfe> %d)%*
.END

The interpretation of a %9λ%*-expression is given in terms of simplification
or conversion rules. To present these rules we need a few definitions.
First a variable, %Dx%*, is  a %2⊗→free variable↔←%* in a <wfe>, %dE%* if:

.BEGIN INDENT 0,10;GROUP;
%dE%* is the variable, %dx%*.

%dE%* is an application, %d(OP A)%*, and %dx%* is free in %dOP%* and %dA%*.

%dE%* is a %9λ%*-expression, %9λ%dy.M%1, if %dx%* is free in %dM%* and %dx%* is
distinct from %dy%*.

.END

The second definition says a variable is a %2⊗→bound variable↔←%* in %dE%*
if it occurs in %dE%* and is not free in %dE%*.
Finally some notation: %dE[...]%* means that %d...%* is a "well-formed"
sub-expression in %dE%*.

There are three %9λ%*-conversion rules which are of interest here:
.BEGIN INDENT 0,10;
.GROUP;

%9α%*-conversion: %dE[%9λ%*x.M]%1 may be converted to %dE[%9λ%*y.M']%1 if %dy%* is not
free in %dM%* and %dM'%* results from %dM%* by replacing every free occurrence
of %dx%* by %dy%*. %9α%*-conversion  allows alphabetic change of free variables.
.APART;
.GROUP;

%9β%1-reduction: %dE[(%9λ%*x.M)N]%1 %9β%*-reducible if no variable which occurs free in %dN%*
is bound in %dM%*. %dE[(%9λ%*x.M)N]%1 is reducible to %dE[M']%* where %dM'%* results
from the replacement of all free occurrences of %dx%* in %dM%* by %dN%*.
Compare  call-by-name on {yon(P98)}.
.APART;
.GROUP

%9∂%1-reduction: We may desire a set of %9∂%*-rules which are associated with the
constants appearing in our %9λ%*-language. Each rule has the basic interpretation:
"%dE%* may always be replaced by %dE'%*." The constants and %9∂%*-reduction
rules are used to construct a %9λ%*-calculus for a specific domain of interest.
.APART

.END
Finally we will say that a  %9λ%*-expression is in (%9β%*, %9∂%*) 
%2normal form%* if
it contains no expression reducible by  %9β%*, or %9∂%* rules.
%9α%*-variants are ignored.
This discussion of %9λ%*-calculi is not meant to be definitive; rather it should
convey the spirit of the subject.  The discussion is complete enough, however,
to suggest some interesting problems for  language design.  First, it is apparent
that there may well be two or more sequences of reductions for a %9λ%*-expression;
is there any reason to believe that these reduction sequences will yield 
the same normal forms?  
Second, if we have two %9λ%*-expressions which reduce
to distinct normal forms, is there any reason to believe that they are
"inherently different" %9λ%*-expressions?


The first question is easier to answer. As we have seen in LISP, the  order
in which calculations are performed can make a difference in the final
outcome.  So too in %9λ%*-calculi. There, however,  we can
show that  if both reduction sequences terminate then they
result in the same normal form. This is usually called the Church-Rosser
theorem. 

The second question obviously requires some explanation of "inherently different".
At one level we might say that by definition, expressions with different
normal forms are "inherently different". 
But a natural interpretation, thinking of %9λ%*-expressions as functions,
is to  say two %9λ%*-expressions are distinct if we can exhibit arguments
such that the value computed by one expression applied to the argument is
different from the value computed by the other. Indeed, for %9λ%*-expressions
which have normal forms, C. Boehm has established this.

What can we say about %9λ%*-expressions which do %2not%* have normal forms?
What if we can exhibit two such %9λ%*-expressions, say %df%* and %dg%*,
 which are distinct
in that no reduction sequence will reduce one to the other, but our
intuition says that they are "the same function". That is, for any
argument, %da%* we supply,  both reductions result in the same expression.
That is %d(f a) = (g a)%*.
The reduction rules of the %9λ%*-calculus cannot help us.
But what should we say if we could
give an interpretation to the %9λ%*-calculus such that in the model our two
wayward expressions have the same meaning? Certainly this should be a convincing
argument for maintaining that they are the "same function" even though
the reduction rules are %2not%* sufficient to display that equivalence 
⊗↓This demonstration also gives credence to the position that the
meaning  transcends the reduction rules.  Compare the incompleteness results
of K. Godel.←.
This, indeed, is the
state of affairs. D. Scott %2has%* exhibited a model or interpretation of
the %9λ%*-calculus, and D. Park has shown the equivalence in this model
of two %9λ%*-expressions which  have distinct  forms.

What does this discussion have to do with language design? Clearly the order of
evaluation or reduction is directly  applicable.  What about the second question?
This is related to the problem of characterization of a language. Do you say that
the language  specification consists of a syntactic component and some
(hopefully precise) description of the evaluation of constructs in that language?
Or do you say that these two components, syntax and a machine, are merely
devices for describing  or formalizing notions about  some abstract  domain of
discourse? The study of formal systems in mathematical logic offers a parallel.
There you are presented with a syntax and a system of axioms and rules of inference.
Most usually we are also offered a "model theory" which gives us models or
interpretations for the syntactic formal system; the model theory usually supplies
additional means of giving convincing arguments for the validity of statements
in the formal system.  Indeed, the arguments made within the formal system
are couched in terms of "provability" whereas arguments of the model theory are
given in terms of "truth". 

C. W. Morris named these three perspectives on language, syntax, pragmatics,
and semantics. I.e.

.BEGIN INDENT 0,10;GROUP;

%2Syntax%*: The synthesis and analysis of sentences in  a language. This area is
well cultivated in programming language  specification.
.APART
.GROUP

%2Pragmatics%*: The relation between the language and its user. 
Evaluators (like %3tgmoaf, tgmoafr, ...%*) come under the heading of pragmatics.
Pragmatics are more commonly referred to as operational semantics in discussions
of programming languages.
.APART
.GROUP

%2Semantics%*: the relation between constructs of the language and the abstract
objects which they denote. This subdivision is commonly referred to as denotational
semantics.

.END

Put differently, syntax describes appearance, pragmatics describes value, and
semantics describes meaning.
Using this classification scheme, most languages are described using syntax, and
a half-hearted pragmatics; seldom does the question of denotation arise.
LISP was described by a syntax and a precise pragmatics; the %9λ%*-calculus
has a simple syntax and  precise pragmatics. The work of D. Scott supplies
a semantics for the %9λ%*-calculus; the work of M. Gordon adapts Scott's work
to LISP. 
Rest assured that we are not persuing formalization simply as an
end in itself. Mathematical notation is no substitute for clear thought,
but we believe careful study of semantics will lead to additional
insights in language design ⊗↓R. D. Tennent has invoked this approach in
the design of %3QUEST%*.←. 

Though the syntax and pragmatics of the %9λ%*-calculus is quite simple, 
and it is a most productive vehicle when used to discuss semantics. 
As we said at the beginning of the section, this calculus was 
intended to explicate the idea of "function" and is therefore a
rarefied discussion of "procedure".
A thorough discussion of the models of the %9λ%*-calculus is beyond the scope of this book,
a few implications are worth mentioning.
There is a reasonably subtle distinction between Church's conception
of a function as a rule of correspondence, and the usual set-theoretic
view of a function as a set of ordered pairs ⊗↓See {yonss(P92)}←.
In the latter setting one rather naturally thinks of the elements of the domain
and range of a function as existing %2prior%* to the construction of the function:
.BEGIN TURN OFF "{","{";
"Let %3f%* be the function {<x,1>, <y,2>, ...}".
.END
Thus in this frame of mind one does not think of functions which can take
themselves as arguments: %3f[f]%*. Such functions are called %2⊗→self-applicative↔←%*.
They are an instance of a common language called procedure-valued variables or
function-valued variables.
See {yonss(P76)} for a discussion of LISP's functional arguments.
The problem on {yon(P99)} is a testimonial to the existence
of self-applicative functions
⊗↓Whether such psychopathic functions are indespensible or even useful
is tangential to our current discussion.  But thinking of language design
it is better to deal with them head on rather than simply rule
them out of existence. They may tell us something about the nature of
procedures (functions), and if past history is any indication, banishment
on such prejudical grounds as "Why would anyone want to do a thing like
that?" will not endure.←

Cast in the %9λ%*-calculus setting, self application is approachable.
The conversion rules of the calculus allow a %9λ%*-expression to be
applied to any  %9λ%*-expression including the expression %2itself%*.
There are well-known logical difficultiies ⊗↓Russell's paradox.← if we allow
unrestricted self-application.
There are then two difficulties. Can we characterize a useful subset of functions
for which self-application is tractable?
Using this subset, can we find a model for the %9λ%*-calculus 
which retains our intuitions about functions. 
The discovery of the appropriate class of functions and the model
construction are two of the important  aspects of D. Scott's work .
We shall not exhibit Scott's constructions, but in {yonss(P85)} we
shall discuss the class of functions.

M. J. C. Gordon has successfully applied Scott's methods to analyze
subsets of LISP. {yonss(P85)} contains some of the ideas in this
recent work.

.SS(Towards a Mathematical Semantics,,P85:)
In {yonss(P15)} we informally introduced some ideas about proving properties
of programs. We would now like to expand on this idea of introducing
mathematical rigor into the discussion of programming languages. Though firm
technical basis can be established for the following discussion, we 
wish to proceed at an intuitive level and hopefully arouse curiosity 
without damaging the underlying theory.

First, why worry about foundational and theoretical work at all? Programming,
it is said, is an art and art needs no formalizing. Indeed, but there is some
science in Computer Science and %2that%* part can be analyzed. 

We have borrowed heavily (but informally) from mathematics and logic; we should
at least see how much of our discussion can stand more formal analysis. We
have used the language of functions and functional composition, but have
noted that not all LISP expressions are to be given a usual mathematical connotation.
In particular, conditional expressions are %2not%* to be interpreted as functional
application. In mathematics, a function is a mapping or set of ordered pairs; 
composition simply denotes a %2new%* mapping or set of ordered pairs. Nothing
is said about how to calculate members of the set of pairs, or indeed, whether
such a set can be effectively (mechanically) given. Can we give an interpretation
to LISP expressions which involves nothing more than the mathematical 
description of function but preserves our LISP-ish intent?

Most of the description of LISP which we have given so far is classified as ⊗→operational↔←.
That means our informal description of LISP and our later description of the LISP
interpreter are couched in terms of "how does it work (operate)". Indeed
the whole purpose of %3eval%* was to describe explicitly what is to happen
when a LISP expression is to be evaluated.  We have seen ({yon(P84)}) that discussion
of evaluation schemes is non-trivial; and that order of evaluation can effect the
outcome ({yon(P17)}).  
.BEGIN TURN ON "#";
.P91:
However, many times the order of evaluation is immaterial
⊗↓One difficulty with the operational approach is that it (frequently)
specifies too much: C. Wadsworth.←. 
We saw on {yon(P93)} that %3eval%* will perform without complaint when
given a form %3f[#...#]%* supplied with too many arguments.
How much of %3eval%* is "really" LISP and how much is "really" implementation.
On one hand we have said that the meaning of a LISP expression %2is%*
(by#definition) what %3eval%* will do to it. On the other hand
it is quite reasonable to claim %3eval%* is simply %2an implementation%*.
There are certainly other implementations; i.e, other functions %3eval%4i%1
which have the same input-output behavior as our %3eval%*. 
The position here is not that %3eval%* is wrong in giving
values to things like %3cons[A;B;C]%*, but rather: just what is it that
%3eval%* implements?

This other way of looking at meaning in programming languages is exemplified by
⊗→denotational↔← or mathematical semantics.
.P96:
This perspective springs from a common mathematical, philosophical, or logical
device of distinguishing between a %2representation%* for an object, and the
object itself. The most usual guise is the numeral-number distinction.
Numerals are notations (syntax) for talking about %2numbers%* (semantics).
thus the Arabic %2numerals%* %32, 02%*, the Roman numeral %dII%*,
and the Binary notation %310%*, all %2denote%* or represent
the %2number%* two. In LISP, %3(A#B), (A#.(B)), (A,B)%* and %3(A#.(B#.#NIL))%*
all are notations for the same symbolic expression, thought of as an abstract object.

We could say that a LISP form %2denotes%* an sexpression (or is undefined) just
as we say in mathematics that 2+2 denotes 4 or 1/0 is undefined. 
Thus %3car[cdr[(A#B)]]%* denotes %3B%* ⊗↓Or more precisely, denotes a symbolic
expression which we represent by %3B%*.←.
The scheme which we use to evaluate the expression
is irrelevant; there is some object which our expression denotes and the process
which we use to discover that object is of no concern. 

Similarly, we will say that
the denotational counterpart of a LISP function or %3prog%* is just a 
(mathematical) function or mapping defined over our abstract domain.
Before  proceeding, discretion dictates the introduction of some conventions
to distinguish notation from %2de%*notation. 
.BEGIN GROUP;
We will continue to use italics:
.BEGIN CENTER;

(%3A, B, ..., x, ... car, ...(A . B) %*) as notation in LISP expressions.
.END
Gothic bold-face:
.BEGIN CENTER;

(%dA, B, ..., x, ...car, ...(A . B)%*) will represent denotations.
.END
.END

Thus %3A%* is notation for %dA%*;
%3car[cdr[(A#B)]]%* denotes %dB%*; the mapping, %dcar%* is the denotation
of the LISP function %3car%*.


.BEGIN TURN OFF "⊗";
The operation of composition of LISP functions denotes mathematical composition;
thus in LISP, %3car[cdr[(A#B)]]%*  means apply the function %3cdr%* to the
argument %3(A#B)%* getting %3(B)%*; apply the function %3car%* to %3(B)%*
getting %3B%*. Mathematically speaking, we have a mapping, %dcar%2⊗%*cdr%1
which is a composition of the %dcar%* and %dcdr%* mappings; the ordered
pair %d<(A#B)#,#B>%* is in the graph of this composed mapping.
%dcar%2⊗%*cdr(#(A#B)#)%1 is %dB%*.
.END
In this setting, any LISP characterization of a function is equally good;
the "efficiency" question has been abstracted
away. But notice that many important properties of real programs %2can%*  be 
discussed in this rarefied mathematical context; 
in particular, questions of equivalence
and correctness of programs are still viable, and indeed, 
more approachable.

Lest your confusion give way to dispair, we should point out that
denotational thinking %2has%* been introduced before.
When we said ({yon(P86)}) that:

.BEGIN CENTERIT;SELECT 3;
←f[a%41%*; ... a%4n%*] = eval[(F A%41%* ... A%4n%*) ...],
.END;
we are guilty of denotational thought. The left hand side of this equation
is denotational; the right hand side is operational.
This denotational-operational distinction is appropriate in a more general context.
When we are presented with someone's program and asked "what does it compute?"
we usually begin our investigation operationally, discovering "what does it %2do%*?".
⊗↓Another common manifestation of this "denotation" phenomonon is the common
programmer complaint: "It's easier to write your own than to understand
someone else's."←
Frequently by tracing its execution we can discover a concise (denotational) description
(E.g.,#"ah!#it#computes#the#square#root.").
.END
The author has already victimized you in this area of denotation and operation. 
When %3great mother%* was presented it was given as an operational exercise,
with the primary intent to introduce the LISP evaluation process without
involving the stigma of complicated names. Forms involving %3great mother%* were 
evaluated perhaps without understanding the denotation, but if asked "what does
%3great mother%* do?" you would be hard pressed to given a comprehensible
purely operational definition. However you might have discovered the true insidious
nature of %3great mother%* yourself; then it would be relatively easy to describe
its (her) behavior. Indeed, once the denotation of %3great mother%* has been discovered
questions like "What is the value of %3tgmoaf[(CAR (QUOTE (A . B)))]%*? " are usually
answered by using the denotation of %3tgmoaf%*: "what is the value of %3car[(A . B)]%*?"
⊗↓The question of how one gives a convincing argument that the successor of %3tgmoaf%*,
(i.e. %3eval%*), %2really does%1 faithfully represent LISP evaluation is the
subject of a recent dissertation by M.J.C. Gordon.←
Finally, for the more practically-minded: the care required in defining a 
denotational model for LISP will  pay dividends in motivating our
extension to LISP in {yonsec(P87)}.

Let us begin to relate these intuitions to our discussion of 
LISP ⊗↓%1This section owes a great deal to M.J.C. Gordon's thesis.
However our presentation is much like that of a person who writes
down a set of axioms, declares that they characterize a particular theory,
but gives no consistency or completeness proofs. Gordon's thesis
contains the necessary substantiation for our light-fingered discussion.←. 
We will parallel  our development of interpreters for LISP since each subset,
%3tgmoaf, tgmoafr%*, and %3eval%*,
will also introduce new problems for our mathematical semantics.
Our first LISP subset considers functions, compostion, and constants.
Constants will be elements of our domain of interpretation.
Clearly, our domain will include
the S-expressions since %2most%* LISP expressions %2denote%* Sexprs. However, we
wish to include more; many of our LISP functions are partial functions. 
It is convenient to be able to talk about the undefined value; in other words we
wish to extend our partial functions on sexprs to be %2total%* functions on
(denotations of) sexprs or "undefined". Our domain
must then include a denotation for "undefined". We will use the symbol %aU%*.
We shall call this extended domain %aS%* (%3≡%*%d<sexpr>%a∪%aU%1)
⊗↓Recall that %d<sexpr>%*'s are simply the denotations of elements in <sexpr>.
I.e.,<sexpr>'s are specific (syntactic) representations; %d<sexpr>%*'s
are abstract objects. Compare the numeral-number discussion on {yon(P96)}.
We could simply muddle the distinction here, but is worthwhile to make a clean
break.←. 

Before we can talk very precisely about the  properties of LISP functions
we must give more careful study to the nature of domains.
Our simplest domain is %d<atom>%*.
It's intuitive structure is quite simple, basically just a set of atoms
or names with no inherent relationships  among the elements.
But what kind on an animal is %d<sexpr>%*?  It's a set of elements, but many
elements are  related. Can we say any more about the characteristics of
%d<sexpr>%*? In our discussion of %d<sexpr>%* beginning on {yon(P47)}
we tried to make it clear that there is more than syntax involved.
Couching that argument in mathematical terminology we could say that
for %ds%41%1 and %ds%42%1 in %d<sexpr>%* then the essence of "dotted pair"
is contained in the concept of the set-theoretic ordered pair, 
<%ds%41%1,%ds%42%1>. Thus the "meaning" of  the set of dotted pairs is
captured by Cartesian product, %d<sexpr>#%ax%*#<sexpr>%1.
Let's continue the analysis of:

.BEGIN CENTERIT;
←<sexpr> ::= <atom> | (<sexpr> . <sexpr>)
.END

We are trying to interpret this BNF equation as a definition of the
domain %d<sexpr>%*. Reasonalbe interpretations of "::=" and "|" appear to
be equality and set-theoretic union, respectively. This results in the
equation:

.BEGIN CENTERIT;SELECT d;
←<sepxr> = <atom> %a∪%* <sexpr> %ax%* <sexpr>
.END

What does this equation mean? It's just like an equation in algebra, and
as such,
it may or may not have  solutions ⊗↓Recall the discussion on {yon(P109)}.←.
Luckily for us, this "domain equation" has a solution: the s-exprs
we all know and love.
There is a natural mapping of BNF equations onto such "domain equations",
and the solutions to the domain equations are sets satisfying 
the abstract essence of the BNF.  The question of existence of solutions,
and indeed the methods involved in obtaining solutions to such equations,
will not be discussed here. The recent studies by D. Scott and C. Strachey
analyze these problems. Most of the foundational work is too advanced
for our discussion.
However, we will persue one very important interpretation of a set of BNF
equations which will demonstrate some of the subtlity 
present in Scott's methods.

Consider the following BNF:
.BEGIN CENTERIT;

←<e> ::= <v> | λ<v>.<e> | (<e> <e>)
.END

These equations comprise a syntax description of the λ-calculus, similar
to that given in {yonss(P49)}.
We would like to describe the natural denotations of these equations in a
style similar to that used for <sexpr>'s.
The  denotations of the expressions, <e>,
 of applications, (<e> <e>), and of the  variables,
<v>, are just constants of the language; call this domain %dC%*.
What should be the denotation of "λ<v><e>"?  A reasonable choice,
consistent with our intuitions of the λ-calculus, is to 
take the set of functions from %dC%* to %dC%*. Write that set as
%dC#→#C%*. Then our domain equation is expressed:

.BEGIN CENTERIT;SELECT d;

←C = C→C
.END
What kind of solutions does this equation have? The answer is easy. It has
absolutely %2no%* interesting solutions! A simple counting argument will establish this.
Unless the domain %dC%* is absolutely trivial, then the number of functions
in %dC#→#C%* is greater than the number of elements in %dC%*.

Does this say that there are no models of the λ-calculus?
We hope not. What it %2should%* say is that our interpretation of "%d→%*"
is too generous. What is needed is an interpretation of functionality
which will allow a solution to the above domain equation; indeed it
should allow a natural interpretation such that the properties which
we expect functions to posses are, in fact, true in the model.
Scott gave one such 
interpretation of "%d→%*" delimiting  what he calls
 the class of "continuous functions.
We will assume without proof that the denotations which we ascribe to
LISP functions in the remainder of this section are in fact continuous.


Then, for example, the
mathematical counterpart to the LISP function %3car%* is the mapping %dcar%* from 
%aS%* to %aS%* defined as follows:

.BEGIN TABIT2(10,20);GROUP


\%dcar:%aS%1→ %*S%1

\\ %1| is %aU%* if %dt%* is atomic
\%dcar(t)\%1< %dt%41%1 if %dt%* is %d(t%41%* . t%42%*)
\\ %1| is %aU%* if %dt%* is %aU%*.

.END
Similar strategy suffices to give denotations for the other primitive LISP functions
and predicates. For example: 

.BEGIN TABIT2(10,20);GROUP


\%datom:%aS%1→ %*S%1

\\ %1| is %dNIL%* if %dt%* is not atomic.
\%datom(t)\%1< is %dT%* if %dt%* is atomic.
\\ %1| is %aU%* if %dt%* is %aU%*.

.END
.BEGIN TURN OFF "{","}";
Notice that %datom%* maps onto a subset of %aS%* rather than a set like {true, false,%aU%*} of
truth values. This behavior is in the spirit of LISP. LISP has already decided to
map truth-values onto the sexpressions %3T%* and %3NIL%*.
.END


Now, corresponding to %3tgmoaf%*, we will have a function, %9D%4tg%1, mapping expressions
onto their denotations. Thus:

.BEGIN TABIT2(30,35);GROUP;TURN ON "#";
\%9D%4tg%1:\<form> => %aS%*.###⊗↓%1Note the difference between "=>" and "→".
The former denotes a map from LISP constructions into denotations;
the latter a map between denotations.←
\\ %3car%1 => %dcar%*
\\   etc. for %3cdr, cons, eq,%1 and%* atom%1.
.END

.BEGIN TURN OFF "{","}";
Before  giving the details of %9D%4tg%1, we need to introduce some notation for
naming elements of the sets <sexpr> and <form>. Let %as%* range over <sexpr>
and %af%* range over <form>, then using  "{" and "}" to enclose LISP constructs
we can write:

.BEGIN centerit;GROUP;

←%9D%4tg%1{%as%*} = %ds%*
←%9D%4tg%1{%3car[%af%*]%1} = %dcar%*(%9D%4tg%1{%af%*})

←with similar entries for %3cdr, cons, eq, %1and %*atom%*.
.END
.END

The similarity with %3tgmoaf%* should be apparent.
.BEGIN TURN ON "#";
The structure of our denotation function, %9D%1, will obviously become more complex
as we proceed. Notice that the denotations for the LISP functions are mappings
such that if any argument is undefined then the value is undefined. That is
%df(#...,%aU%*,#...)%1 is %aU%*. Such mapping are called %2⊗→strict↔←%*.
This is as it should be: forms %3f[e%41%*,#...,#e%4n%*]%1 are undefined if
any %3e%4i%1's are undefined. As we will see, there are natural mappings which are
%2not%* strict; i.e., they can  give a value other that %aU%* even when an argument
is %aU%*.

Let's now continue with the next subset of LISP, adding conditional
expressions to our discussion. As we noted on {yon(P88)}, a degree of care need
be taken if we attempt to interpret conditional expressions in terms of mappings.
First we simplify the problem slightly; it is easy to show that a general
LISP conditional can be expressed in terms of the more simple expression,
[p%41%*#→#e%41%*;#%3T%*#→#e%42%*]%1.
Now, using our extended domain, %aS%*, it %2is%* reasonable to think
of conditional expressions as function applications in the mathematical
sense ⊗↓Obviously, the order of evaluation of arguments to the conditional
expression will have been "abstracted out". But recall the comment of Wadsworth
({yon(P91)}). Indeed, the use of conditional expressions in the more
abstract representations of LISP functions frequently is such that 
exactly one of the p%4i%*'s is %3T%* and all the others are %3NIL%*.
Thus in this setting, the order of evaluation of the predicates is useful 
for "efficiency" but not necessary to maintain the sense of the definition.
See {yon(P101)}.←.
Consider [p%41%*#→#e%41%*;#%3T%*#→#e%42%*]%1 as denoting %dcond(p%41%*,e%41%*,e%42%*)%1
where:

.BEGIN TABIT2(10,22);GROUP
\%dcond: %aS%*x%aS%*x%aS%* → %aS%*

\\ %1| is%* y %1if%* x %1is%* %dT%*
\%dcond(x,y,z)\%1< is %dz%1, if %dx%1 is %dNIL%*.
\\ %1| is %aU%1, otherwise
.END
.END

This interpretation of conditional expressions is appropriate for LISP; other
interpretations of conditionals are possible. For example:

.BEGIN TABIT2(10,24);GROUP
\%dcond%41%*: %aS%*x%aS%*x%aS%* → %aS%*

\\ %1| is%* y %1if%* x %1is%* %dT%*
\%dcond%41%*(x,y,z)\%1< is %dz%1, if %dx%1 is %dNIL%*.
\\ %1| is %aU%1 if %dx%* is %aU%* and %dy ≠ z%*
\\ %1| is %dy%1 if %dx%* is %aU%* and %dy = z%*
.END

Notice neither %dcond%* or %dcond%41%1 are strict mappings.
Now to add (simplified) conditionals to %9D%4tg%1, yielding %9D%4tgr%1:
.BEGIN TABIT1(12);TURN OFF "{","}";FILL;
\%9D%4tgr%1{%3[%af%41%3 → %af%42%3; T → %af%43%3]%1} = 
%dcond(%9D%4tgr%1{%af%41%1}%d,%9D%4tgr%1{%af%42%1}%d,%9D%4tgr%1{%af%43%1}%d)%1
.END

As with the LISP evaluators, nothing particularly novel appears until we
begin consideration of variables. What is the denotation of a variable? 
As we know, the value of a LISP <variable> ({yon(P66)})  depends on the 
current environment or symbol table. Denotationally, things
really don't differ much from  the discussion of %3eval%*. All we need
do ⊗↓This statement is a bit too optimistic!← is give a mathematical 
representation of environments.
As a reasonable first attempt we can try characterizing environments as
functions from variables to sexpressions; i.e.:

.BEGIN CENTER
%denv %1is the set of functions: <%dvariable%*> → %aS%1.
.END

.BEGIN TURN ON "#";
Indeed, this is essentially the argument used in introducing %3assoc%* ({yonss(P92)}).
Note too, that %3assoc[x;l]#=#%dl(x)%1 is another instance of a 
operational-denotational relationship. We will exploit this remark in a moment.
.END

.BEGIN TURN OFF "{","}";
So, given a LISP variable, %3x%*, and a member of %denv%*, say 
the function %d{<x,2>,<y,4>}%*, then
our newest %9D%* should map %3x%* onto %d2%*. This is an intuitive way of saying
that %9D%* should map a member of <variable> onto a %2function%*. This function
should map a member of %denv%* onto an element of %aS%*. Now to make things more precise.
.END


.BEGIN TABIT2(30,35);TURN OFF "→";
\%9D%*:\<variable> => [%denv%* → %aS%*]
.END

.BEGIN TURN OFF "{","}";TURN ON "#";

Thus for example: %9D%*{%3x%*}(%d{<x,2>,<y,4>}%1)#=#%d2%*.
Introducing %av%* as a meta-variable to range over <variable>, 
then for %dl#%9ε%d#env%1 we have:

.CENTER;
%9D%1{%av%*}%d(l)%*#=#%dl(v)%1
.END
We should then say that the %2meaning%* or denotation of a variable is a function;
whereas the %2value%* of a variable is an element of %aS%1.

Alas, our present description of %denv%* is inadequate. %denv%* is
to represent symbol tables; such tables must include function names
and their defintions. Function names, like <variable>s, are in the class
<identifier>; so in the interest of simplicity %denv%* should map from
%d<identifier>%* to ...; to what? What are the denotations of LISP 
functions? Clearly they should be mathematical functions or mappings.

.BEGIN TURN ON "#";
So letting
%aFn%* be the set of functions:#%9S%4n=0%1[%aS%8n%1#→#%aS%1],
and %aId%1 be %d<identifier>%1∪%aU%1,
then a more realistic approximation to %denv%* is:
.BEGIN CENTER
%denv%1 is the set of functions: %aId%1 → %aS%1 ∪ %aFn%1.
.END
.END
That is, an element of %denv%* is a function which maps an identifier
either onto a s-expression or onto a function from s-expressions to s-expressions.
We shall soon see that even this is  inadequate.
Meanwhile, let's continue expanding %9D%*.

We shall maintain the parallels between evaluation and denotation, by giving
%9D%4e%1 and %9D%4a%1 corresponding to %3eval%* and %3apply%*.
.BEGIN TABIT2(20,26);TURN OFF "→";GROUP;
Thus: \%9D%4e%1:\<form> => [%denv%* → %aS%*] and 
\%9D%4a%1:\<function> => [%denv%* → %aFn%*].

.END
We must also make consistent modifications to the previous clauses of %9D%4tgr%1 to
account for environments. For example:
.BEGIN TURN OFF "{","}";TURN ON "#";
%9D%4e%1{%as%*}(%dl%*)#=#%ds%*. That is, the value of a constant is independent of the
specific environment in which it is evaluated. The simple modification for
conditional expressions is left to the reader.
.END
Some of the more obvious properties of %9D%4a%1 hold:
.BEGIN TURN OFF "{","}";

.BEGIN CENTER;
%9D%4a%1{%3car%1}%d(l)%1 = %dcar%*
.END

.BEGIN TURN ON "{","}";
Similar equations hold for the other LISP primitive functions and predicates.
To mimic look-up of a variable used as a function name we propose: ⊗↓This is
not a sufficient characterization.←
.END
.CENTER;

%9D%4a%1{%af%*}%d(l)%* = %dl(f)%*, where %af%* %9ε %1<function>.
.END
To describe the evaluation of a function-call in LISP we must add
an equation to %9D%4e%1:
.BEGIN TURN OFF "{","}";TABIT1(15);FILL;TURN ON "#";

\%9D%4e%1{%af%*[%as%41%1,#...,%as%4n%1]}%d(l)%1#=#
%9D%4a%1{%af%1}%d(l)(%9D%4e%1{%as%41%1}%d(l)%1,#...,%9D%4e%1{%as%4n%1}%d(l))%1
.END

Clearly, before we get very far in applying functions to values
we must give a mathematical characterization of function definitions.
We will do this in five (increasingly complex) steps. First
we  handle λ-notation without free variables; 
next, %3label%* definitions without free variables;
then λ-notation involving free variables;
explication of  recursive definitions in denotational semantics comes next; and
finally we examine recursion in the presence of free variables.

First, 
what should be the denotation of %3λ[[x%41%*, ..., x%4n%*] %9x%1] 
⊗↓Assuming the only free variables in %9x%* are among the %3x%4i%*'s.← in an
environment? Intuitively, it should be a function, and recalling 
({yon(P93)}) that %3eval%* expects n-ary
LISP functions be supplied with at %2least%* n arguments, it should
be a function from %aS%9*%1 to %aS%* such that:
.BEGIN TURN OFF "{","}";TABIT1(15);FILL;TURN ON "#";

\%9D%4a%1{λ[[%av%41%1,#...#%av%4n%1]%as%1]}%d(l)%1#=#
%d%9λ%d(x%41%*,#...,#%dx%4n%*)%9D%4e%1{%as%1}%d(l#:#<x%41%*,%dv%41%d>,#...,#<x%4n%*,%dv%4n%d>)%1
.END

.BEGIN TURN ON "#";
where λ is the LISP λ-notation and %9λ%* is its mathematical counterpart. 
%dv%4i%1 is the denotational counterpart of %av%4i%1.

In more detail:
%9λ%d(x%41%*, ... ,x%4n%*)e(x%41%*, ... ,x%4n%*) %1is a function %df%*: %aS%8n%1 → %aS%* such that:

.BEGIN TABIT1(15);GROUP;

\ | is %de(t%41%*, ... ,t%4n%*) %1if m%c≥%*n and %c∀%*i%dt%4i%1 %c≠%* %aU%1.
%df(t%41%*, ... t%4m%*)  %1\<
\ | is %aU%* otherwise

.END
Also, %d(l#:#<x%41%*,%dv%41%d>,#...,#<x%4n%*,%dv%4n%d>)%1 is a modification
of %dl%* such that each %dv%4i%1 is bound to  the corresponding %dx%4i%1.

.BEGIN TABIT1(20);GROUP;
That is: 
%d(l#:#<x,v>)%1 is: %9λ%d(v%41%*)%2\if %dv = %aU%* %2then %aU%2 
\else if %dv%41%* = %aU%2 then %aU%2
\else if %dv%41%* = x%2 then %dv%2
\else %dl(v%41%*)%1.

where: %2if%d p%* then %dq%* else %dr%1  is  %dcond(p,q,r)%1.
.END

Now let's begin to clarify the mathematical content of the operator, "<=".
The device we use in LISP to name functions is %3label%*. Though {yonss(P90)} makes it
clear that a simple-minded approach is doomed, let's see how far it %2will%* go.
As before, we take our clues from the behavior of %3eval%* and %3apply%*.
In any environment %9D%4a%1 should map %3label[f;g]%* in such a way that the 
denotation of %3f%* is synonymous with that of %3g%*.
That is, %df%* is a mapping satisfying the equation 
%df(t%4i%*,#...,#t%4n%*)#=#%dg(t%4i%*,#...,#t%4n%*)%1.
So:
.END

.BEGIN TURN OFF "{","}";CENTERIT;FILL;TURN ON "#";
←%9D%4a%1{%3label[%af%1;%ag%*]}%d(l)%1#=#%9D%4a%1{%ag%1}%d(l)%1.
.END

This will suffice for our current λ-definitions; we need not modify %dl%*
since the name %3f%* will never be used within the evaluation of 
an expression involving %3g%*.

.BEGIN TURN ON "#";
By now you should be getting suspicious that all is not quite right. We will
now justify your discomfort. First, our proposed description of the meaning
of λ-notation is a bit too cavalier. Our treatment of evaluation of free
variables in LISP (on {yon(P93)} and in {yonss(P77)}) shows that free
variables in a function are to be evaluated when the function is %2activated%*
and %2not%* when the function is defined. Thus a λ-definition generally
requires an environment in which to evaluate its free variables.
So its denotation 
should be a mapping like: %denv%*#→#[%aS%9*%1#→#%aS%*] rather than
simply %aS%9*%1#→#%aS%1. Is this consistent with our understanding of the
meaning of λ-notation? Yes. 
It is exactly what %2⊗→closure↔←%* was attempting to 
describe. What we previously have called an ⊗→open function↔← is a creature of the
form: 
 %aS%9*%1#→#%aS%*.

.END
 This enlightened view of λ-notation must change our conception on %denv%* as well.
Now, given a name for a function in an environment we can expect to receive
a mapping from %denv%* to an element of %aFn%*. I.e. for such names:

.BEGIN CENTERIT;
←%denv %1is the set of functions: %aId%1 → [%denv%1 → %aFn%1]
.END
We will let you ponder the significance of this statement for a few moments
while we continue the discussion of "<=".

A modification of our handling of %3label%* seems to describe the case 
for recursion:

.BEGIN TURN OFF "{","}";CENTERIT;FILL;TURN ON "#";
←%9D%4a%1{%3label[%af%1;%ag%*]}%d(l)%1#=#%9D%4a%1{%ag%1}%d(l#:#<f,%9D%4a%1{%ag%1}%d>)%1.
.END

Interpreting this equation operationally, it says: when we apply a %3label%*
expression in an environment it is the same as applying the body of the definition
in an environment modified to  associate the name with its definition.
This is analogous to what the LISP %3apply%* function will do.

Recalling the inadequacy of this interpretation of %3label%* in more
general contexts ({yon(P94)}),
we should perhaps look further for a general reading of %3label%*. Our hint
comes from our interpretation of "<=" as an equality. I.e., recall:

.BEGIN CENTER;SELECT 3;TURN OFF "←";

fact ← %1a solution to the equation:%* f = λ[[x][x=0 → 1; T → *[x;f[x-1]]]].
.END
What we need is a representation of an "equation-solver" which will
take such an equation as input and will return as value a function
which satisfies that equation. In particular we would like the %2best%* 
solution in the sense that it requires the minimal structure on the function.
⊗↓Like a free group satisfies the group axioms, but imposes no other
requirements.← 
This request for minimality translates to finding the function which
satisfies the equation, but is least-defined on other elements of the
domain. Though a full discussion of "least" brings in the recent work of D. Scott
and is a bit too advanced for our purposes, the intuition behind
this study is quite accessible and again illuminates the distinction
between mathematical meaning (denotational) and manipulative meaning (operational).
Consider the following LISP definition:

.BEGIN CENTER;SELECT 3;

f <= λ[[n][n=0 → 0; T → f[n-1] + 2*n -1]]
.END

.BEGIN TURN ON "#";
When we are asked what this function is doing, most of us would proceed
operationally; that is, we would begin computing %3f[n]%* for different
values of %3n%* --what#is#%3f[0]?%*,
 what is %3f[1]%1,#...#. It is profitable to look at this process differently:
what we are doing is looking  at a %2sequence%* of functions,
call them %df%4i%1's .
.END

.BEGIN TABIT3(10,16,44);SELECT d;GROUP;TURN OFF "{","}";

\f%40%1 =\%d{<0,%aU%*>,<1,%aU%*>, ... }\%1when we begin, we know nothing.
\%df%41%1 =\%d{<0,0>,<1,%aU%*>, ... }\%1now we know one pair.
\%df%42%1 =\%d{<0,0>,<1,1>, ... }\%1now two
\%df%43%1 =\%d{<0,0>,<1,1>,<2,4>, ... }\%1now three

\ ...\           ...          ...\%dEureka!!
.END

When (if) the sudden realization strikes us that the LISP function is
"really" (denotationally)  %dn%82%1 on the non-negative integers, 
then we may either take
that insight on faith or subject it to proof. The process of discovering
the denotation  can be construed as a limiting process which creates 
the least-defined function satisfying the LISP definition. That is:

.BEGIN CENTER;SELECT d;

%9λ%d((n)n%82%d)%1 = %1least upper bound of%d f%4i%1's;
.END
where %df%4i%1 may also be characterised as:

.BEGIN TABIT1(12);SELECT D;group;

\ %1|%d n%82%1 if %d0%c≤%dn%c≤%di
f%4i%d(n)%1 =\<
\ | %aU%1 if %di%c<%dn

.END

We may think of our "equation-solver" as proceding in such a manner.
Though it is not at all obvious, such an equation solver
%2does%* exist; it is called the %2⊗→fixed-point operator↔←%* and is 
designated here by %dY%*. We will now give an intuitive derivation of %dY%*.
Interpreting this equation operationally, it says: when we apply a %3label%*
expression in an environment it is the same as applying the body of the definition
in an environment modified to  associate the name with its definition.
This is analogous to what the LISP %3apply%* function will do.

Recalling the inadequacy of this interpretation of %3label%* in more
general contexts ({yon(P94)}),
we should perhaps look further for a general reading of %3label%*. Our hint
comes from our interpretation of "<=" as an equality. I.e., recall:

.BEGIN CENTER;SELECT 3;TURN OFF "←";

fact ← %1a solution to the equation:%* f = λ[[x][x=0 → 1; T → *[x;f[x-1]]]].
.END
What we need is a representation of an "equation-solver" which will
take such an equation as input and will return as value a function
which satisfies that equation. In particular we would like the %2best%* 
solution in the sense that it requires the minimal structure on the function.
⊗↓Like a free group satisfies the group axioms, but imposes no other
requirements.← 
This request for minimality translates to finding the function which
satisfies the equation, but is least-defined on other elements of the
domain. Though a full discussion of "least" brings in the recent work of D. Scott
and is a bit too advanced for our purposes, the intuition behind
this study is quite accessible and again illuminates the distinction
between mathematical meaning (denotational) and manipulative meaning (operational).
Consider the following LISP definition:

.BEGIN CENTER;SELECT 3;

f <= λ[[n][n=0 → 0; T → f[n-1] + 2*n -1]]
.END

.BEGIN TURN ON "#";
When we are asked what this function is doing, most of us would proceed
operationally; that is, we would begin computing %3f[n]%* for different
values of %3n%* --what#is#%3f[0]?%*,
 what is %3f[1]%1,#...#. It is profitable to look at this process differently:
what we are doing is looking  at a %2sequence%* of functions,
call them %df%4i%1's .
.END

.BEGIN TABIT3(10,16,44);SELECT d;GROUP;TURN OFF "{","}";

\f%40%1 =\%d{<0,%aU%*>,<1,%aU%*>, ... }\%1when we begin, we know nothing.
\%df%41%1 =\%d{<0,0>,<1,%aU%*>, ... }\%1now we know one pair.
\%df%42%1 =\%d{<0,0>,<1,1>, ... }\%1now two
\%df%43%1 =\%d{<0,0>,<1,1>,<2,4>, ... }\%1now three

\ ...\           ...          ...\%dEureka!!
.END

When (if) the sudden realization strikes us that the LISP function is
"really" (denotationally)  %dn%82%1 on the non-negative integers, 
then we may either take
that insight on faith or subject it to proof. The process of discovering
the denotation  can be construed as a limiting process which creates 
the least-defined function satisfying the LISP definition. That is:

.BEGIN CENTER;SELECT d;

%9λ%d((n)n%82%d)%1 = %1least upper bound of%d f%4i%1's;
.END
where %df%4i%1 may also be characterised as:

.BEGIN TABIT1(12);SELECT D;group;

\ %1|%d n%82%1 if %d0%c≤%dn%c≤%di
f%4i%d(n)%1 =\<
\ | %aU%1 if %di%c<%dn

.END

We may think of our "equation-solver" as proceding in such a manner.
Though it is not at all obvious, such an equation solver
%2does%* exist; it is called the %2⊗→fixed-point operator↔←%* and is 
designated here by %dY%*. We will now give an intuitive derivation of %dY%*.

In terms of our example we want a solution to %df = %9t%d(f)%1, where:

.BEGIN CENTER;
%9t%d(g) = %9λ%d((n) cond(n=0, 0, g(n-1)+2*n-1))%1,
.END

Our previous discussion leads us to believe that
%9λ%d((n)n%82%d) %1for %dn %c≥%d0%1 is the desired solution.

.BEGIN TURN ON "#";

How does this discussion relate to the sequence of functions %df%4i%1?
First, it's important to keep the domains of our various mapping in mind:
%df%*#%9ε%*#Fn and %9t%* is a functional in %aFn%1#→#%aFn%1.
Let's look at the behavior of %9t%* for various 
arguments. The simplest function is the totally undefined function, %aU%*#⊗↓We 
perhaps should subscript %aU%* to distinguish it from previous %aU%*'s.←.


.BEGIN CENTER;
%9t%d(%aU%*) = %9λ%d((n) cond(n=0, 0, %aU%*(n-1)+2*n-1))%1,
.END
but this says %9t%d(%aU%*)%1 is just %df%41%1!
Similarly,
.BEGIN CENTER;
%9t%d(%9t%d(%aU%*))#=#%9λ%d((n) cond(n=0, 0, f%41%*(n-1)+2*n-1))%1,
.END
is just %df%42%1.
Thus, writing %9t%8n%1 for the composition of %9t%1...%9t%1, n times, ⊗↓Define
%9t%80%1 to be the the totally undefined function, %aU%1.← we can say
.BEGIN CENTER;GROUP;

%df%4n%* = %9t%8n%d(%aU%*)%1  or,

%9λ%d((n)n%82%*)%1 = lim%4n=0 → ∞%9t%8n%d(%aU%d)%1.
.END

Or in general the fixed-point of an equation %df = %9t%*(f)%1 satisfies the
relation:

.BEGIN CENTER;

%dY(%9t%*) = lim%4n→∞%9t%8n%d(%aU%d).%1
.END
Thus in summary, %dY%* is a mapping:[%aFn%* → %aFn%*] → %aFn%*
such that if %9t%*#%9ε%*#[%aFn%*#→#%aFn%*] and %df%*#=#%9t%d(f)%1, then
%9t%d(Y(%9t%*))%1#=#%dY(%9t%*)%1 and %dY(%9t%*)%1 is least-defined of any of the solutions
to %df%*#=#%9t%d(f)%1.
.END

So the search for denotations for %3label%* might be better served by:

.BEGIN TURN OFF "{","}";CENTERIT;FILL;TURN ON "#";
←%9D%4a%1{%3label[%af%1;%ag%*]}%d(l)%1#=
#%dY(%9λ%d(h)%9D%4a%1{%ag%*}%d(l%1#:#%d<f,h>))%1.
.END


Which characterization of %3label[f;g]%* is "better"?
The first denotation parallels the behavior of %3eval%* and %3apply%*, applying
%3g%* in a %denv%* modified by  the pair %d<f,g>%*.
The later fix-point characterization says %3label[f;g]%* is a particular
solution the the equation %3f=g%*. As we have seen, the "meaning" of %3label%*
is better served by this fix-point interpretation. The crucial questions, however,
are: first, are these two  denotations different? 
And which, if either, interpretation is %2correct%*? 
That is, which
characterization has the same %2effect%* as %3eval%* and %3apply%*?
.BEGIN TURN OFF "{","}";TURN ON "#";
First, the characterizations are %2not%* the same. Examination of the
behavior of %9D%4e%1{%3label[car;car][(A#B)]%1} will exhibit a discrepancy.
.END

The general question of the correctness of the denotational semantics which we
are developing is the subject of much of M. Gordon's thesis.

***add lisp induction***


The intuitions presented in this section can be made very  precise. 
The natural ordering
of "less defined" exemplified by the sequence of %df%4i%1's: %df%4i%1 is less
defined (or approximates) %df%4j%1, j%c≥%1i, imposes a structure on our domain of functions.
Indeed, a structure can be naturally superimposed on all of our domains.
If we require that some additional simple properties hold on our domains, then
the intuitions of this section can be justified mathematically.

*** ADD MONOTONICITY, CONTINUITY

The papers of Scott, Gordon, and Wadsworth supply the missing precision.
In case you think least fixed points are too removed from the realities of
programming language design, please refer to {yon(P94)} again.
Though intuition finally uncovered a counterexample to the general application
of the specific implementation of LISP's %3label%*, intuition has been guilty
of superficiality here. The nature of recursion is a difficult question and
this fixpoint approach should make us aware of the pitfalls.


Actually we glossed over a different kind of fixed point a few moments
ago:

.BEGIN CENTERIT;
←%denv%1 is the set of functions  %aId%1 → [%denv%1 → %aFn%1]
.END

This statement requires a fixed point interpretation to be meaningful.
Finally stirring denotations for simple variables back into our %denv%*,
we are led to an adequate description of environments for LISP:

.BEGIN CENTERIT;
←%denv%1 is the set of functions  %aId%1 → [%denv%1 → %aFn%1∪%aS%1]
.END

**structure of domains**

**justification**

Recalling that  this characterization of %denv%* arose in explicating
free variables, it should  not come as too much of a suprise that
we must modify the fix-point characterization of %3label[f;g]%*.
We had assumed that %3f%* and %3g%* were in %aFn%*, whereas they are
in %denv%*→%aFn%1. %3label[f;g]%* binds %3f%* to %3g%* in an environment,
leaving free variables in %3g%* unassigned. These free variables of %3g%*
are evaluated in the environment current when the %3label%*-expression
is applied. Thus the meaning of a %3label%*-expression should also be a
member of %denv%*→%aFn%1. So:

.BEGIN TURN OFF "{","}";CENTERIT;FILL;TURN ON "#";
←%9D%4a%1{%3label[%af%1;%ag%*]}%d(l)%1#=
#%dY(%9λ%d(h)(%9λ%d(l%9*%d)(%9D%4a%1{%ag%*}%d(l%9*%1#:#%d<f,h>)) ))(l)%1.
.END

Notice that all our work on fixed-points  and recursion equations has only
involved %2single%* equations. Indeed, the label operator can only define
a single function. Frequently a function needs to be defined via a %2set%*
of recursion equations. In particular when we wrote %3eval%* and %3apply%*
we were really asking  for the solution  to such a set of equations: %2⊗→mutual recursion↔← equations%*.
When we wrote:

.BEGIN TABIT1(30);SELECT 3;GROUP;
\eval <= λ[[e;a] ... 
\apply <= λ[[fn;x;a] ...
.END

As we said in {yonss(P38)}, we really meant:

.BEGIN TABIT1(30);SELECT 3;GROUP;
\label[eval; λ[[e;a] ... ]
\label[apply; λ[[fn;x;a] ...]
%1 where %3eval%* and %3apply%* occur within the %3λ%*-expressions.
.END

That is:
.BEGIN TABIT1(30);SELECT 3;GROUP;
\label[eval; %9F%1(%3eval,apply%1)]
\%3label[apply; %9Q%1(%3eval,apply%1)]
.END

Now since LISP doesn't allow %3label%* to express mutual recursion directly,
we must resort to a subterfuge if we wish to express such constructions in LISP.

Namely:
.BEGIN CENTER;SELECT 3;

label[eval; %9F%1(%3eval,label[apply; %9Q%1(%3eval,apply%1)]%1)]

.END

Clearly this subterfuge is applicable to the definition of other
(mutually recursive) functions; but subterfuge, it is. To really be
useful, we realize that LISP must at least allow a %2sequence%* of
definitions to be given such that these definitions will be in effect
through some  reasonable calculation. 
There is minimal insight gained by thinking
of our LISP functions as anonymous solutions to a gigantic fixpoint equation.
Sequencing, thus is important. Sequencing is implicit in the order
of evaluation of arguments expressed in %3eval%*; sequencing is 
implicit in the evaluation of ⊗→special form↔←s. 
Certainly sequencing has become quite explicit by the time we examine %3prog%*.
All of these  manifestations of sequencing have been abstracted out in the
denotational approach. 
It is natural to ask whether there is  some way to introduce
sequencing into our formalism so that more realistic implementations
can be proved correct.

***continuations: extensions to sequencing and order of evaluation***

After all this work there really should be a comparable return on
on our investment. We believe there is. An immediate benefit is
clearer understanding of the differences between mathematics and programming
languages. 
A clearer perception of the role of definition and computation.
Later we will see that the thought required to specify domains and 
ranges of functions is directly applicable to 
the design of an extension to LISP which allows user-defined
data structures.



.CENT(Problems);
%2I%*  What is the %2statement%* of the correctness of %3eval%* in terms
of the denotational semantics?